|
| 1: |
|
minus(x,0) |
→ x |
| 2: |
|
minus(s(x),s(y)) |
→ minus(x,y) |
| 3: |
|
quot(0,s(y)) |
→ 0 |
| 4: |
|
quot(s(x),s(y)) |
→ s(quot(minus(x,y),s(y))) |
| 5: |
|
app(nil,y) |
→ y |
| 6: |
|
app(add(n,x),y) |
→ add(n,app(x,y)) |
| 7: |
|
reverse(nil) |
→ nil |
| 8: |
|
reverse(add(n,x)) |
→ app(reverse(x),add(n,nil)) |
| 9: |
|
shuffle(nil) |
→ nil |
| 10: |
|
shuffle(add(n,x)) |
→ add(n,shuffle(reverse(x))) |
| 11: |
|
concat(leaf,y) |
→ y |
| 12: |
|
concat(cons(u,v),y) |
→ cons(u,concat(v,y)) |
| 13: |
|
less_leaves(x,leaf) |
→ false |
| 14: |
|
less_leaves(leaf,cons(w,z)) |
→ true |
| 15: |
|
less_leaves(cons(u,v),cons(w,z)) |
→ less_leaves(concat(u,v),concat(w,z)) |
|
There are 12 dependency pairs:
|
| 16: |
|
MINUS(s(x),s(y)) |
→ MINUS(x,y) |
| 17: |
|
QUOT(s(x),s(y)) |
→ QUOT(minus(x,y),s(y)) |
| 18: |
|
QUOT(s(x),s(y)) |
→ MINUS(x,y) |
| 19: |
|
APP(add(n,x),y) |
→ APP(x,y) |
| 20: |
|
REVERSE(add(n,x)) |
→ APP(reverse(x),add(n,nil)) |
| 21: |
|
REVERSE(add(n,x)) |
→ REVERSE(x) |
| 22: |
|
SHUFFLE(add(n,x)) |
→ SHUFFLE(reverse(x)) |
| 23: |
|
SHUFFLE(add(n,x)) |
→ REVERSE(x) |
| 24: |
|
CONCAT(cons(u,v),y) |
→ CONCAT(v,y) |
| 25: |
|
LESS_LEAVES(cons(u,v),cons(w,z)) |
→ LESS_LEAVES(concat(u,v),concat(w,z)) |
| 26: |
|
LESS_LEAVES(cons(u,v),cons(w,z)) |
→ CONCAT(u,v) |
| 27: |
|
LESS_LEAVES(cons(u,v),cons(w,z)) |
→ CONCAT(w,z) |
|
The approximated dependency graph contains 7 SCCs:
{19},
{24},
{25},
{16},
{17},
{21}
and {22}.